Section: New Results

Model-Checking Reactive Probabilistic Systems

Participant : Rohit Chadha.

Rohit Chadha along with A. Prasad Sistla and Mahesh Viswanathan continued their study on reactive probabilistic systems modeled as Probabilistic Büchi Automata (PBA) in [30] . Reactive probabilistic systems are probabilistic non-deterministic systems in which the nondeterminism is resolved by a external environment which is oblivious of the “current" state of the system. This paper investigates the power of PBA when the threshold probability of acceptance is non-extremal, i.e., is a value strictly between 0 and 1. Many practical randomized algorithms are designed to work under non-extremal threshold probabilities and thus it is important to study power of PBAs for such cases. The paper presents a number of surprising expressiveness and decidability results for PBAs when the threshold probability is non-extremal. Some of these results sharply contrast with the results for extremal threshold probabilities. The paper also presents results for Hierarchical PBAs and for an interesting subclass of them called simple PBAs.

Rohit Chadha along with V. Korthikranthi, M. Viswanathan, G. Agha and Y. Kwon also study reactive probabilistic systems in [28] . In  [28] , reactive probabilistic systems are viewed as transformers of probability distributions, giving rise to a labeled transition system over the probability distributions over the states of the system. Thus, a reactive probabilistic system can be seen as defining a set of executions where each execution is a sequence of probability distributions. Reasoning about sequences of distributions allows one to express properties not expressible in standard probabilistic logics like PCTL; examples include expressing bounds on transient rewards and expected values of random variables, as well as comparing the probability of being in one set of states at a given time with another set of states. With respect to such a semantics, the model-checking problem is undecidable. In this paper, the authors identify a special class of systems called semi-regular Markov Decision Processes that have a unique non-empty, compact, invariant set of distributions, for which they show that checking any $\omega$-regular property is decidable. Their decidability result also implies that for semi-regular probabilistic finite automata with isolated cut-points, the emptiness problem is decidable.